[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification suffix-array-ops
enrich suffix-array with
   procedures 
      create_suffixarray#  array : suffixarray nondeterministic;
declaration 
   create_suffixarray# (ar; sar)
     { 
        sar := mksuffixarray(# ar) ; 
        let n = 0 in while n < # sar do { 
                                           sar := sar[n, n] ; n := n + 1
                                        } ; 
        sort#(λ n0, n1. suffix(ar, n0) < suffix(ar, n1) ∨ suffix(ar, n0) = suffix(ar, n1); sar)
     };
end enrich